(VAR x y)
(RULES
+(0,x) -> x
+(s(x),y) -> s(+(x,y))
*(0,x) -> 0
*(s(x),y) -> +(y,*(x,y))
)